\begin{tabbing}
input{-}forwarding\=\{i:l\}\+
\\[0ex](${\it es}$; ${\it Cmd}$; ${\it Sys}$; ${\it isupdate}$; ${\it In}$; $f$)
\-\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=$\forall$$e$:E(${\it Sys}$).\+
\\[0ex](($\uparrow$($e$ $\in_{b}$ ${\it In}$)) $\Rightarrow$ (${\it Sys}$($e$) = [${\it In}$($e$)]))
\\[0ex]\& (\=($\neg$($\uparrow$($e$ $\in_{b}$ ${\it In}$)))\+
\\[0ex]$\Rightarrow$ ($\neg$(loc($f$($e$)) = loc($e$)))
\\[0ex]$\Rightarrow$ \=((($\exists$${\it e'}$:E(${\it Sys}$). ((${\it e'}$ $<$loc $e$) \& loc($f$(${\it e'}$)) = loc($f$($e$)))) $\Rightarrow$ (${\it Sys}$($e$) = ${\it Sys}$($f$($e$))))\+
\\[0ex]\& (\=($\neg$($\exists$${\it e'}$:E(${\it Sys}$). ((${\it e'}$ $<$loc $e$) \& loc($f$(${\it e'}$)) = loc($f$($e$)))))\+
\\[0ex]$\Rightarrow$ (\=${\it Sys}$($e$)\+
\\[0ex]=
\\[0ex]if $e$ $\in_{b}$ prior(${\it Sys}$)
\\[0ex]then nth\_tl(\=$\parallel$filter\=(${\it isupdate}$\+\+
\\[0ex];es{-}interface{-}history(${\it es}$; ${\it Sys}$; prior(${\it Sys}$)($e$)))$\parallel$;
\-\\[0ex]filter(${\it isupdate}$;es{-}interface{-}history(${\it es}$; ${\it Sys}$; ($f$($e$)))))
\-\\[0ex]else filter(${\it isupdate}$;es{-}interface{-}history(${\it es}$; ${\it Sys}$; ($f$($e$))))
\\[0ex]fi ))))
\-\-\-\-\\[0ex]\& (($\neg$($\uparrow$($e$ $\in_{b}$ ${\it In}$))) $\Rightarrow$ (loc($f$($e$)) = loc($e$)) $\Rightarrow$ (${\it Sys}$($e$) = []))
\\[0ex]\& (\=did{-}forward(${\it es}$; ${\it Sys}$; $f$; $e$)\+
\\[0ex]$\Rightarrow$ \=($\forall$$a$:E(${\it Sys}$).\+
\\[0ex]($a$ $<$loc $e$)
\\[0ex]$\Rightarrow$ should{-}forward(${\it es}$; ${\it In}$; ${\it isupdate}$; $f$; $a$)
\\[0ex]$\Rightarrow$ did{-}forward(${\it es}$; ${\it Sys}$; $f$; $a$)))
\-\-\-
\end{tabbing}